\begin{tabbing}
cr{-}effective(${\it es}$;${\it Sys}$;${\it Out}$;$f$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=${\it e'}$:es{-}E{-}interface(${\it es}$;${\it Sys}$)\+
\\[0ex]$\exists$\=${\it e''}$:es{-}E{-}interface(${\it es}$;${\it Out}$)\+
\\[0ex](fun{-}connected(es{-}E{-}interface(${\it es}$;${\it Sys}$);$f$;${\it e'}$;$e$) \& es{-}le(${\it es}$;${\it e'}$;${\it e''}$))
\-\-
\end{tabbing}